Specification node-index-restrict

[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

enrich
   node-index
, 
   key-order
with
   

   
   
   functions  . |≤ . : node-index × key → node-index prio 9 left;
              . |> . : node-index × key → node-index prio 9 left;
   
   
   
   
   

   

   axioms in-le :  ⊦ key0 ∈ ri |≤ key1 ↔ key0 ∈ ri ∧ ¬ key1 < key0;
          used for: s, ls;
          at-le :  ⊦ ¬ key1 < key0 ∧ key0 ∈ ri → (ri |≤ key1)[key0] = ri[key0];
          used for: s, ls;
          in-gt :  ⊦ key0 ∈ ri |> key1 ↔ key0 ∈ ri ∧ key1 < key0;
          used for: s, ls;
          at-gt :  ⊦ key1 < key0 ∧ key0 ∈ ri → (ri |> key1)[key0] = ri[key0];
          used for: s, ls;

   

   
end enrich